Contracts & Harnesses for widening_mul #111
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Towards : issue #59
Parent branch : main
Revalidation :
Per the discussion in #59, we have to build and run Kani from feature/verify-rust-std branch.
To revalidate the verification results, run the following command. <harness_to_run> can be either num::verify to run all harnesses or num::verify::<harness_name> (e.g. widening_mul_u16_small) to run a specific harness.